1. Field of the Invention
This invention pertains generally to digital circuit design and particularly to combinational equivalence verification.
2. Background of the Invention
Today's logic circuits are so complex that circuit designers must use computer-based techniques to help them in their task. Some of these techniques transform a specification of a circuit into an equivalent implementation of the circuit. During this transformation, errors may be introduced into the implementation. Accordingly, checking must be performed to verify that the implementation conforms with the specification. Combinational equivalence checking is one form of checking.
When applied to a pair of sequential circuits, combinational equivalence checking typically consists of two steps: latch mapping and verification. The first step constructs a latch mapping (also known as a register mapping) by identifying corresponding latches in the two designs to be compared. Then, it is possible to break the circuits into corresponding combinational blocks (e.g., single-output, multiple-input Boolean functional blocks). The second step is to verify whether the corresponding combinational blocks are equivalent. If the corresponding blocks are equivalent, the circuits are functionally equivalent.
There has been much research on the second step, verification. For example, A. Kuehlmann and F. Krohm, "Equivalence Checking Using Cuts and Heaps," DAC, 1997, and D. K. Pradhan, D. Paul, and M. Chatterjee, "VERILAT: Verification Using Logic Augmentation and Transformations," ICCAD, 1996, are recent examples. However, there has been little research on the first step, constructing a latch mapping.
Existing commercial tools for constructing a latch mapping use heuristics based on signal names or circuit structure. However, tools that perform design transformations such as synthesis or clock tree insertion often do not preserve signal names, especially when a design is flattened as part of the transformation. If two combinational blocks are found to be inequivalent, it may be because of an incorrect latch mapping rather than a bug in the circuit. This possible error in the latch mapping complicates debugging.
Accordingly, there is a need for a method and system for constructing a latch mapping that accurately maps corresponding latches in the two circuit designs. Preferably, the method and system should not use heuristics based on signal names or circuit structure to construct the latch mapping.